es:event_system{i:l}, i,x:Id, T:Type. @i discrete fpf-single(x; T)  es-dtype(es; i; x; T) 

latex

Definitions	t  T, x:A. B(x), es-dtype(es; i; x; T), Id, False, Type, prop{i:l}, s = t, left + right, P  Q, x:A  B(x), event_system{i:l}, atom{$n:n}, b, void, <a, b>, es-vartype(es; i; x), P  Q, eq_id(a; b), x:AB(x), P  Q, P  Q, P  Q, x.A(x), guard(T), x. t(x), ff, bor(p; q), fpf-ap(f; eq; x), fpf-dom(eq; x; f), fpf-all(A; eq; f; x,v.P(x;v)), fpf-single(x; v), @i discrete ds, sq_type(T), sqequal(s; t)
Lemmas	Id sq, event system wf, iff functionality wrt iff, iff transitivity, assert of bor, bor wf, bfalse wf, all functionality wrt iff, implies functionality wrt iff, or functionality wrt iff, assert-eq-id, assert wf, eq id wf, false wf, Id wf, es-dtype wf